[Lucas - PLILP'96, Example 3.12]

Example 3.12 in [Lucas - PLILP'96]

Summary: Ex3_12_Luc96a

CS-TRS Ex3_12_Luc96a (file Ex3_12_Luc96a.csr)

Functions:  from cons s sel 0

Constructors:  cons s 0

Variables:  X Y Z

Arities: 

ar(from) = 1
ar(cons) = 2
ar(s) = 1
ar(sel) = 2
ar(0) = 0

Replacement map: 

µ(from)={1}
µ(cons)={1}
µ(s)={1}
µ(sel)={1,2}
µ(0)={}

Rules: (file Ex3_12_Luc96a)

from(X) -> cons(X,from(s(X)))
sel(0,cons(X,Y)) -> X
sel(s(X),cons(Y,Z)) -> sel(X,Z)

The CS-TRS in OBJ format (file Ex3_12_Luc96a.obj):

obj Ex3_12_Luc96a is
  sort S .
  op from : S -> S .
  op cons : S S -> S [strat (1 0)] .
  op s : S -> S .
  op sel : S S -> S .
  op 0 : -> S .
  vars X Y Z : S .
  eq from(X) = cons(X,from(s(X))) .
  eq sel(0,cons(X,Y)) = X .
  eq sel(s(X),cons(Y,Z)) = sel(X,Z) .
endo

Negative results

  1. The µ-termination of Ex3_12_Luc96a cannot be proved by using Lucas' transformation. The TRS Ex3_12_Luc96a_L: 
        from(X) -> cons(X)
    sel(0,cons(X)) -> X
    sel(s(X),cons(Y)) -> sel(X,Z)
    contains extra variables (see [Luc98, Section 4.1]).
  • The µ-termination of Ex3_12_Luc96a can not be proved by using CSDP

    Positive results

    1. Ex3_12_Luc96a is proved µ-terminating in [Zan97, Example 2] by using the following interpretation: 
          [0] = 1
    [s](x) = x + 1
    [cons](x,y) = x + (y div 2)
    [from](x) = 2x + 4
    [sel](x,y) = (2^x)y
    2. Ex3_12_Luc96a is proved µ-terminating in [Zan97, Example 3] by using Zantema's transformation. The TRS Ex3_12_Luc96a_Z: 
          from(X) -> cons(X,n__from(s(X)))
    sel(0,cons(X,Y)) -> X
    sel(s(X),cons(Y,Z)) -> sel(X,activate(Z))
    from(X) -> n__from(X)
    activate(n__from(X)) -> from(X)
    activate(X) -> X
      is terminating (use LPO with AProVE).
    3. By [GM04, Theorem 11], the µ-termination of Ex3_12_Luc96a can also be proved by using Ferreira and Ribeiro's transformation (but no concrete proof has been reported yet).
    4. By [GM04, Theorem 22], the µ-termination of Ex3_12_Luc96a can also be proved by using Giesl and Middeldorp's transformation (but no concrete proof has been reported yet).
    5. The µ-termination of Ex3_12_Luc96a can also be proved by using CSRPO (computed with MuTerm).
    6. Proved µ-terminating by using a polynomial interpretation over Q_1 [Luc04, Example 8] 
          [0] = 1
    [s](x) = 2x 
    [cons](x,y) = x + y/4
    [from](x) = 2x + 2
    [sel](x,y) = (x^2)y + 1
      An analogous interpretation can also be (computed with MuTerm)